1. Technical Field
The present invention relates to integrated circuit verification tools in general, and more particularly, to a method and system for performing equivalence checking on logic circuits. Still more particularly, the present invention relates to a method and system for performing ternary verification.
2. Description of Related Art
Binary modeling is a common framework for evaluating logic designs. With binary modeling, logic gates in the form a hardware design representation are evaluated with 0,1 valuations. For example, when evaluating an AND gate, if any of its input signals is a logical 0, then the AND gate should evaluate to a logical 0; otherwise, the AND gate should evaluate to a logical 1. Given a set of 0,1 valuations to the primary inputs of a netlist, a simple deterministic binary simulation algorithm can be used to evaluate the 0,1 valuations to all gates within the netlist.
Ternary modeling evaluates logic designs with 0,1,X valuations, where X represents an “unknown” condition. Given a set of 0,1,X valuations to the primary inputs of a netlist, a simple deterministic algorithm can be used to evaluate the logic gates within the netlist with ternary modeling. For example, when evaluating an AND gate, if any of its input signals is a logical 0, then the AND gate should evaluate to a logical 0; however, if none of its input signals is a logical 0 while one of its input signals is X, then the AND gate should evaluate to X.
Ternary modeling has several practical benefits. First, if used effectively, ternary modeling can effectively double the coverage of binary evaluation for every X that is injected in place of a logical 0 or 1 input value. For example, if simulating a data-independent property of a logic circuit design, a circuit designer may simulate 0,1 values to the control inputs, and X values to all data inputs of a logic circuit design. If a run has N input valuations that take the X value, and if a property under consideration can be consistently evaluated in that ternary simulation (such as the run does not become inconclusive by propagating X values to the signals being checked with the property), such run correlates to 2N binary simulations.
Second, a circuit designer may automatically infer properties with ternary modeling. For example, a circuit designer may verify that a particular Xed input valuation does not propagate or persist in a netlist by checking the downstream logic does not evaluate to X. In contrast, when using binary evaluation, such a property will not be as simply expressed.
Third, in equivalence checking applications, a circuit designer may validate that one model refines the other by checking not just that a set of signals of one logic design always evaluate to the same values in the other, but by relaxing the equality check so that equality of signals (as well as conditions where one model exhibits an X but the other exhibits a 0,1 value) are accepted.
Despite all its advantages, ternary modeling has a significant drawback. In order to accommodate a three-valued interpretation of an inherent binary netlist, each gate in the binary netlist must be modeled with two gates. This results in inefficiencies during ternary evaluation. Consequently, it would be desirable to provide an improved method and system for performing ternary verification.